(declare-const x Float32)
(declare-const y Float32)
(assert (and (fp.isNormal x) (fp.isNormal y)))
(assert (and (fp.leq ((_ to_fp 8 24) RNE 1.0) x) (fp.leq x y) (fp.leq y ((_ to_fp 8 24) RNE 2.0))))
(declare-const xy32 Float32)
(assert (= xy32 (fp.mul RNE x y)))
(declare-const xy64 Float64)
(assert (= xy64 (fp.mul RNE ((_ to_fp 11 53) RNE x) ((_ to_fp 11 53) RNE y))))
(assert (fp.isNormal ((_ to_fp 8 24) RNE xy64)))
(declare-const hi Float32)
(declare-const lo Float32)
(assert (= hi (fp.mul RNE x y)))
(assert (= lo (fp.fma RNE x y (fp.neg hi))))
(declare-const xy Float64)
(assert (= xy (fp.add RNE ((_ to_fp 11 53) RNE hi) ((_ to_fp 11 53) RNE lo))))
(assert (not (= xy64 xy)))
(check-sat)
